\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $L_{1}$, $L_{2}$, $L$:($T$ List), $x$:$T$.\+
\\[0ex]no\_repeats($T$;$L$) $\Rightarrow$ $L_{1}$ @ [$x$] $\subseteq$ $L$ $\Rightarrow$ [$x$ / $L_{2}$] $\subseteq$ $L$ $\Rightarrow$ $L_{1}$ @ [$x$ / $L_{2}$] $\subseteq$ $L$
\-
\end{tabbing}